COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00015 ENDMK
C⊗;

;;;;......
7. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP FLAT(X~Y,U)
))⊃
    (∀X U.LISTP FLAT(X,U))
   deps: NIL

* 
(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil| sortinfo)

1 is the only part of a bound expression.
*  failed to derive 
∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP FLAT(X,FLAT(Y,U)
))

cannot prove the following: 
(∀U.LISTP FLAT(Y12,U))∧(∀U.LISTP FLAT(X25,U))⊃LISTP FLAT(X25,FLAT(Y12,U30)
)

* 
(rw * |([1#1#2]($definfo**sortinfo))**simpinfo*nil*([1](der))*nil|
 sortinfo)
EKL Done.
proof? 
* proof? 
* Done.
LISPAX read in 
proof? 
* FLAT started.
* 
* 1. NIL
   deps: NIL

* 2. ∀X U.FLAT(X,U)=IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))
   deps: NIL

* 
* 4. NIL
   deps: NIL

* 5. ∀X.FLATTEN(X)=IF ATOM X THEN LIST(X) ELSE FLATTEN(CAR X)*FLATTEN(CDR 
X)
   deps: NIL

* 
* 
;;;
(wipe-out)
(get-proofs lispax)
(proof flat)
(context lispax#1:*)

;;; flat(x,u) has an imbedded call which makes proofs more difficult.
(decl (flat) |ground⊗ground→ground| constant)

(axiom |∀x u.flat(x,u) = if atom x then x~u else flat(car x,flat(cdr x, u))|)
(lname definfo)

(decl (flatten) |ground → ground| constant)

(axiom |∀x.flatten(x) = if atom x then list(x)
                        else flatten(car x)*flatten(cdr x)|)
(lname definfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO**SORTINFO))*NIL*([1#2#1#2]($DEFINFO**SORTINFO))*
  *SIMPINFO*NIL*([1](DER))*NIL| SORTINFO)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil*([1](der))*nil|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil|
 sortinfo)

(∀e phi |λx.listp flatten(x)| sexpinduction
|nil*([1#1#1]($definfo*nil**simpinfo*nil))*nil
*([1#1#2](&definfo*nil**simpinfo*nil))*([1#1](imp(listappend)*der))*nil|
 sortinfo)
(lname listpflatten)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil
*([1#1#2](&definfo**simpinfo*nil))|
listpflatten sortinfo)

(assume |(∀u.flat(x,u)=flatten(x)*u)∧(∀u.flat(y,u)=flatten(y)*u)|)

(trw |flat(x,flat(y,u))| |*-1| listpflatten sortinfo)

(∀i u)

(ci -3 -1)

(∀i (x y))

(trw |∀x u.flat(x,u) = flatten(x)*u| |imp(-6,-1)*taut|)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo**simpinfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo**simpinfo*nil))*nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil
*([1#1#2](&definfo**simpinfo))|
listpflatten sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))*nil|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))*sortinfo*nil|
 sortinfo)

;;;;
(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil*([1](der))*nil|
 sortinfo)